$\forall$$T$, $A$:Type, $a$, $x$:Id, $f$:($A$$\rightarrow$$T$), ${\it tg}$:Id, $l$:IdLnk, ${\it es}$:ES.
\\[0ex]locl($a$) sends [${\it tg}$,$f$\{$A$$\rightarrow$$T$\}($x$)] on link $l$ once $\in$ Prop